|
In mathematics, a Heyting algebra is a bounded lattice (with join and meet operations written ∨ and ∧ and with least element 0 and greatest element 1) equipped with a binary operation ''a'' → ''b'' of ''implication'' such that ''c'' ∧ ''a'' ≤ ''b'' is equivalent to ''c'' ≤ ''a'' → ''b''. From a logical standpoint, ''A'' → ''B'' is by this definition the weakest proposition for which modus ponens, the inference rule ''A'' → ''B'', ''A'' ⊢ ''B'', is sound. Equivalently a Heyting algebra is a residuated lattice whose monoid operation ''a''⋅''b'' is ''a'' ∧ ''b''; yet another definition is as a posetal cartesian closed category with all finite sums. Like Boolean algebras, Heyting algebras form a variety axiomatizable with finitely many equations. Heyting algebras were introduced by to formalize intuitionistic logic. As lattices, Heyting algebras are distributive. Every Boolean algebra is a Heyting algebra when ''a'' → ''b'' is defined as usual as ¬''a'' ∨ ''b'', as is every complete distributive lattice satisfying a one-sided infinite distributive law when ''a'' → ''b'' is taken to be the supremum of the set of all ''c'' for which ''a'' ∧ ''c'' ≤ ''b''. The open sets of a topological space form such a lattice, and therefore a (complete) Heyting algebra. In the finite case every nonempty distributive lattice, in particular every nonempty finite chain, is automatically complete and completely distributive, and hence a Heyting algebra. It follows from the definition that 1 ≤ 0 → ''a'', corresponding to the intuition that any proposition ''a'' is implied by a contradiction 0. Although the negation operation ¬''a'' is not part of the definition, it is definable as ''a'' → 0. The definition implies that ''a'' ∧ ¬''a'' = 0, making the intuitive content of ¬''a'' the proposition that to assume ''a'' would lead to a contradiction, from which any other proposition would then follow. It can further be shown that ''a'' ≤ ¬¬''a'', although the converse, ¬¬''a'' ≤ ''a'', is not true in general, that is, double negation does not hold in general in a Heyting algebra. Heyting algebras generalize Boolean algebras in the sense that a Heyting algebra satisfying ''a'' ∨ ¬''a'' = 1 (excluded middle), equivalently ¬¬''a'' = ''a'' (double negation), is a Boolean algebra. Those elements of a Heyting algebra of the form ¬''a'' comprise a Boolean lattice, but in general this is not a subalgebra of H (see below). Heyting algebras serve as the algebraic models of propositional intuitionistic logic in the same way Boolean algebras model propositional classical logic. Complete Heyting algebras are a central object of study in pointless topology. The internal logic of an elementary topos is based on the Heyting algebra of subobjects of the terminal object 1 ordered by inclusion, equivalently the morphisms from 1 to the subobject classifier Ω. Every Heyting algebra whose set of non-greatest elements has a greatest element (and forms another Heyting algebra) is subdirectly irreducible, whence every Heyting algebra can be made an SI by adjoining a new greatest element. It follows that even among the finite Heyting algebras there exist infinitely many that are subdirectly irreducible, no two of which have the same equational theory. Hence no finite set of finite Heyting algebras can supply all the counterexamples to non-laws of Heyting algebra. This is in sharp contrast to Boolean algebras, whose only SI is the two-element one, which on its own therefore suffices for all counterexamples to non-laws of Boolean algebra, the basis for the simple truth table decision method. Nevertheless, it is decidable whether an equation holds of all Heyting algebras.〔Kripke, S. A.: 1965, ‘Semantical analysis of intuitionistic logic I’. In: J. N. Crossley and M. A. E. Dummett (eds.): Formal Systems and Recursive Functions. Amsterdam: North-Holland, pp. 92–130.〕 Heyting algebras are less often called pseudo-Boolean algebras, or even Brouwer lattices, although the latter term may denote the dual definition, or have a slightly more general meaning. == Formal definition == A Heyting algebra ''H'' is a bounded lattice such that for all ''a'' and ''b'' in ''H'' there is a greatest element ''x'' of ''H'' such that : This element is the relative pseudo-complement of ''a'' with respect to ''b'', and is denoted ''a''→''b''. We write 1 and 0 for the largest and the smallest element of ''H'', respectively. In any Heyting algebra, one defines the pseudo-complement ¬''a'' of any element ''a'' by setting ¬''a'' = (''a''→0). By definition, , and ¬''a'' is the largest element having this property. However, it is not in general true that , thus ¬ is only a pseudo-complement, not a true complement, as would be the case in a Boolean algebra. A complete Heyting algebra is a Heyting algebra that is a complete lattice. A subalgebra of a Heyting algebra ''H'' is a subset ''H''1 of ''H'' containing 0 and 1 and closed under the operations ∧, ∨ and →. It follows that it is also closed under ¬. A subalgebra is made into a Heyting algebra by the induced operations. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Heyting algebra」の詳細全文を読む スポンサード リンク
|